COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	That a function is iterative is an extensional property of the
C00004 ENDMK
C⊗;
That a function is iterative is an extensional property of the
functional.  Let's write it as a logical formula

∀x.(tau(bottom,x)≠bottom ∨ ∃y.(y≠bottom ∧ ∀f.(tau(f,x) = f(y))))

The next step should be to go from this to the formula for the
inductive assertion method - namely

we can then assert that tau has the form

tau(f,x) = if p x then g(x) else f h x.

The inductive assertion method then says

∀x.(P x ∧ ¬ p x ⊃ P h x) ∧ ∀x.(P x ∧ p x ⊃ Q g x) ⊃ ∀x.(P x ⊃ Q f x)

This should be a consequence of the minimization schema

∀x.(phi x ≥≥ tau(phi, x)) ⊃ ∀x.(phi x ≥≥ f x).

All this requires elaboration for the general case of inductive assertions
in which there is a set of mutually recursive functions.  The generalization
is presumably straightforward.

	More than this seems to be required before we can claim that the
observation that the iterative character of the program is an extensional
property of tau is useful.